1. Technical Field
This disclosure relates to electronic design automation (EDA). More specifically, this disclosure relates to parallel evaluation of temporal assertions during property verification by formal means or by simulation.
2. Related Art
The importance of circuit verification cannot be over-emphasized. Indeed, without circuit verification it would have been impossible to design complicated integrated circuits which are commonly found in today's computing devices.
One form of verification typically uses two types of logical expressions: assumptions and assertions. Assumptions are logical expressions that are used primarily in formal verification to model the runtime environment of a design-under-verification (DUV) by constraining the input sequences to only those that are legally allowed to be provided to the DUV. Without assumptions, the DUV may not be constrained to legal behavior, and the assertions being verified may be incorrectly falsified. Assertions are logical expressions that define the desired behavior of the DUV. For example, in some approaches, a circuit is simulated, and during the simulation, a set of assertions is evaluated to verify that the circuit is functioning correctly.